package tableaux.rules;

import java.util.HashSet;
import java.util.Set;

import kb.TBox;

import tableaux.*;
import tableaux.backjumping.DependencyImp;
import tableaux.backjumping.DependencyImpMax;
import tableaux.blocking.BlockingStrategy;
import utils.exception.CoreReasoningException;

import entities.*;
import entities.concept.*;
import entities.role.Role;

public class RuleExists {

	public static boolean print = false;
	private ExistsConcept nextExp;
	private Completion dc;
	private Branching br;
	private final TBox tb;

	public RuleExists(Completion dc) {
		super();
		this.dc = dc;
		this.br = this.dc.getCurrentBranching();
		this.tb = this.dc.getInitTBox();
	}

	// public boolean labelSeenBefore(Individual n){
	// //for(Individual nn:Individual.getAllIndividuals().values()){
	// for(Individual nn:this.dc.getInitABox().getABoxIndividuals()){
	// if(nn.getOrder() < n.getOrder() &&
	// nn.getLabels().containsAll(n.getLabels())
	// && n.getLabels().containsAll(nn.getLabels())){
	// return true;
	// }
	// }
	// return false;
	// }

	public boolean isApplicable(Individual n) {
		boolean app = false;
		try {
			if (n.isBlockable() && (n.isBlocked() || BlockingStrategy.canBeBlocked(n, dc.getInitTBox()))) {
				// make sure it is not blocked
				return false;
			}
		} catch (CoreReasoningException e) {
			e.printStackTrace();
		}
		for (Concept c : n.getLabels()) {
			if (n.getExpandedLabels().contains(c)) {
				continue;
			}
			if (c instanceof ExistsConcept) {
				ExistsConcept ec = (ExistsConcept) c;
				Role r = ec.getRole();
				Concept filler = ec.getFiller();
				// applicable only if no safe neighbors such that (R, filler)
				if (n.hasSafeNeighbor(r, filler, dc.getInitTBox())) {
					continue;
				}
				this.nextExp = ec;
				app = true;
				break;
			}
		}
		return app;
	}
	

	public boolean applyRule(Individual n) {
		boolean specialNominalRule = false;
		boolean suc = false;
		Role r = this.nextExp.getRole();
		// two imps
		Set<Integer> ndep = null;
		Integer singledep = 0;
		if (Completion.DEP_MAX) {
			singledep = DependencyImpMax.getDepOfConcept(n, nextExp);
		} else {
			ndep = DependencyImp.getDepSetOfConcept(n, nextExp);
		}
		Concept filler = this.nextExp.getFiller();
		// non merging reasoning
		if (!Completion.MergeNominal && conjunctNominal(filler)) {
			// return this.applyRuleNominalSpecial(n);
			specialNominalRule = true;
		}
		//get all domain/range concepts to be added for this individual
		//need to add the domain of this role and all superroles!
		for(Concept dmc : r.getCompleteDomain(this.tb.getRoleBox())){
			if(!n.getLabels().contains(dmc)){
				boolean rasuc = n.addLabels(dmc);
				// dep for domain concept
				if (Completion.DEP_MAX) {
					DependencyImpMax.addDep(n, dmc, singledep);
				} else {
					DependencyImp.setDep(n, dmc, ndep);
				}
				if (rasuc && BranchChanges.getRecordingStatus()) {
					br.getBranchChanges().addToLabel(n, dmc);
				}
				suc = true;
			}
		}

		Individual temp = null;
		if (specialNominalRule) {
			Nominal nom = nomsToBeCreated.iterator().next();
			temp = nom.getAttachedInstanceForExistsRule();
		} else {
			temp = Individual.getAnonIndividual();
			// add generating parent
//			temp.setGeneratingParent(n);
//			if (BranchChanges.getRecordingStatus()) {
//				br.getBranchChanges().addGeneratingParent(temp);
//			}
		}
		temp.setGeneratingParent(n);
		if (BranchChanges.getRecordingStatus()) {
			br.getBranchChanges().addGeneratingParent(temp);
		}
		//
		if (print)
			System.err.println(this.nextExp + " creates " + temp.getName());
		// add dependency, temp is generated by Ex R.filler in node n
		if (Completion.DEP_MAX) {
			temp.addGeneratedByDepMax(singledep);
		} else {
			temp.addGeneratedByDep(ndep);
		}

		//
		Set<Concept> labelsToTemp = new HashSet<Concept>();
		temp.addLabels(filler);
		labelsToTemp.add(filler);
		// add dependency for filler
		if (Completion.DEP_MAX) {
			DependencyImpMax.addDep(temp, filler, singledep);
		} else {
			DependencyImp.setDep(temp, filler, ndep);
		}
		// DependencyImp.setDep(temp, filler, ndep);
		for(Concept rgc: r.getCompleteRange(this.tb.getRoleBox())){
			if(!n.getLabels().contains(rgc)){
				if (Completion.DEP_MAX) {
					DependencyImpMax.addDep(temp, rgc, singledep);
				} else {
					DependencyImp.setDep(temp, rgc, ndep);
				}
				// DependencyImp.setDep(temp, rgc, ndep);
				boolean rasuc = temp.addLabels(rgc);
				if (rasuc)
					labelsToTemp.add(rgc);
			}
		}
		Role ir = this.tb.getRoleBox().getInverseRole(r);
		// brand new relations established, no need to check if previous
		// relations exist.
		boolean api = n.addParents(ir, temp);
		boolean acr = n.addChild(r, temp);
		boolean apr = temp.addParents(r, n);
		boolean aci = temp.addChild(ir, n);
		boolean expadd = n.addExpandedLabels(this.nextExp);
		// successor always added to the head of queue
		boolean addsuc = dc.addToQueue(temp,
				Completion.InQueueOrder.INQUEUEFIRST);
		if (BranchChanges.getRecordingStatus()) {
			BranchChanges brc = br.getBranchChanges();
			brc.addToLabel(temp, labelsToTemp);
			if (addsuc) {
				brc.updateQueueInds(temp, 1);
			}
			if (acr)
				brc.updateRoleRelations(n, r, temp,
						BranchChanges.modType.ADD_CHILD);
			if (api)
				brc.updateRoleRelations(n, ir, temp,
						BranchChanges.modType.ADD_PARENT);
			if (aci)
				brc.updateRoleRelations(temp, ir, n,
						BranchChanges.modType.ADD_CHILD);
			if (apr)
				brc.updateRoleRelations(temp, r, n,
						BranchChanges.modType.ADD_PARENT);
			if (expadd)
				brc.addToExpandedLabel(n, this.nextExp);
		}
		// if this concept is expanded after any other already expanded forall
		// concepts
		// temp.restoreForallConceptToExpandedLabels(ir);
		n.restoreForallConceptToExpandedLabels(r, this.tb.getRoleBox());
		suc |= true;
		return suc;
	}

	// filler = Nom and DEF and ...
	private Set<Nominal> nomsToBeCreated = null;

	private boolean conjunctNominal(Concept filler) {
		nomsToBeCreated = new HashSet<Nominal>();
		if (filler instanceof AndConcept) {
			AndConcept cs = (AndConcept) filler;
			// if(cs.getConceptSet().size() == 2){
			for (Concept c : cs.getConceptSet()) {
				if (c instanceof Nominal) {
					nomsToBeCreated.add((Nominal) c);
				}
			}
			// }
		}
		return nomsToBeCreated.size() == 1;
	}

}
